es:ES, A:Type, X:AbsInterface(A), P:(A), e:E. ((e  X|a.P(a)))  (X|a.P(a)(e) ~ X(e)) 

latex

Definitions

E, x:AB(x), b, s ~ t, P  Q, x:A. B(x), s = t, t  T, , Type, ES, Top, left + right, do-apply(f;x), can-apply(f;x), X(e), X|a.P(a), e  X, AbsInterface(A), f(a), False, A, inl x , , , inr x , outl(x), ff, True, x(s), b, x:A  B(x), P & Q, P  Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), p  q, p  q, p q, tt, , Unit, <a, b>, let x,y = A in B(x;y), t.1, x:A.B(x), Void, (x  l)

Lemmas

eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, true wf, false wf, event system wf, top wf, bool wf, assert wf, es-E wf